A, B:Type, f:(A(B + Top)), P:(A), p:(x:A. Dec(P(x))), x:A.
(can-apply(p-co-restrict(f;p);x))  ((can-apply(f;x)) & (P(x))) 

latex

ProofTree

Definitions	Type, , x:A. B(x), t  T, True, x:AB(x), P  Q, P  Q, x. t(x), f(a), x(s), T, Top, left + right, p-co-filter(f), do-apply(f;x), can-apply(f;x), , b, x:A  B(x), P & Q, P  Q, Void, False, A, Dec(P), if b then t else f fi , Unit, ff, tt, case b of inl(x) => s(x) | inr(y) => t(y), A c B, S  T, suptype(S; T), inl x , inr x , s = t, x:A.B(x), x.A(x), f o g  , p-co-restrict(f;p)
Lemmas	decidable wf, iff functionality wrt iff, can-apply-compose-iff, p-compose wf, false wf, not wf, p-co-filter wf, do-apply wf, btrue wf, bfalse wf, bool wf, squash wf, true wf, top wf, can-apply-p-co-filter, assert wf, can-apply wf, do-apply-p-co-filter